/*
 * Slicer.h
 *
 *  Created on: Nov 16, 2010
 *      Author: xavier
 */

#ifndef SLICER_H_
#define SLICER_H_

#include "klee/Interpreter.h"
#include "klee/Internal/Module/KInstruction.h"
#include "klee/Internal/Module/KModule.h"
#include "llvm/Analysis/PostDominators.h"

#include <map>
#include <vector>
#include <list>
#include <queue>
using namespace std;
using namespace klee;

namespace klee {

	//Xiaowei: trace entry
	struct TraceEntry {
		KInstruction * kins; //point to klee instruction
		KFunction * kfun; //point to klee function
		std::vector< ref<Expr> > operandsvalues; //operand value
		std::vector< ref<Expr> > operandsvalues_concrete;
		ref<Expr> destvalue; //instruction value
		ref<Expr> destvalue_concrete; //instruction value
		KInstruction * ret_addr; //point to klee instruction
		int pid;
		unsigned long instance; //instruction instance
		unsigned long long id;
		std::set < TraceEntry *> defuse; //def use graph edge
		std::set < TraceEntry *> usedef; //use def graph edge
		TraceEntry * caller;
	};

	struct SlicerExploitParser : public cl::basic_parser<unsigned long long> {
	      // parse - Return true on error.
	      bool parse(cl::Option &O, llvm::StringRef ArgName, llvm::StringRef Arg,
	                 unsigned long long &Val);
	};

	struct LiveEntry {
		int pid;
		KFunction * kfun;
		int * oprand;
		ref<Expr> value;
		int type;
	};



	struct tecomp {
	  bool operator() ( TraceEntry * const & lhs, TraceEntry * const& rhs) const
	  {return lhs->id < rhs->id;}
	};

	class Slicer {
	private:
		//first is the instruction, second is the instance count
		std::map <KInstruction *, long> kins_db;
		std::vector <TraceEntry *> trace;
		std::set <TraceEntry *, tecomp> slice;
		std::list <LiveEntry *> live;
		std::map<TraceEntry *, std::set<TraceEntry* >, tecomp > trace_live;
		unsigned long long ins_count;
		TraceEntry * cur_te;
		std::map<uint64_t, TraceEntry *> shdwmem;
		PostDominatorTree * pdt;
		FunctionPassManager * fpm;

	public:
		Slicer () {
			ins_count = 0;
			cur_te = 0;
		}
		long addKinsToDB (KInstruction * kins);
		void addToTrace(TraceEntry * entry);
		void incCount(){ins_count++;}
		unsigned long long getCount() {return ins_count;}
		void printTrace (raw_ostream & out);
		void printInsDB ();
		void run(TraceEntry * exploit);
		int mayWriteF(TraceEntry * te);
		int mayWrite(TraceEntry * te);
		int writtenBetween(TraceEntry *, TraceEntry *);
		int isPostDominate (TraceEntry *, TraceEntry *);
		void takeToSlice(TraceEntry *);
		void updateWritten(TraceEntry *);
		void addReadtoLive(TraceEntry *);
		void printTraceEntry(TraceEntry *, raw_ostream & out);
		void writeShdwmem(uint64_t, TraceEntry *);
		void buildDSlice(TraceEntry * exploit);
		void printSlice(raw_ostream & out);
		void initRequiredPass(Module *m);
		std::vector<TraceEntry *>::reverse_iterator findCall (TraceEntry * ret, std::vector<TraceEntry *>::reverse_iterator start);
		int isConcrete(TraceEntry * te);
		PostDominatorTree * getPDT() {return pdt;}
		TraceEntry * readShdwmem(uint64_t);
		void set_cur_te(TraceEntry * te)
		{
			this->cur_te = te;
		}
		TraceEntry * get_cur_te(void)
		{
			return cur_te;
		}
	};

}
#endif /* SLICER_H_ */
